$\forall$$i$:Id. onceR\{a:ut2, done:ut2\}($i$) $\in$ es\_realizer\{i:l\}